\contentsline {chapter}{Abstract}{ii}{section*.1}
\contentsline {chapter}{List of Tables}{v}{chapter*.3}
\contentsline {chapter}{List of Figures}{vi}{chapter*.4}
\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.5}
\contentsline {section}{\numberline {1.1}Motivation}{1}{section.6}
\contentsline {section}{\numberline {1.2}Contribution}{2}{section.7}
\contentsline {section}{\numberline {1.3}Organization of this thesis}{3}{section.8}
\contentsline {chapter}{\numberline {2}Previous Work}{4}{chapter.9}
\contentsline {chapter}{\numberline {3}$\pi $ Calculus}{7}{chapter.10}
\contentsline {section}{\numberline {3.1}Introduction}{7}{section.11}
\contentsline {section}{\numberline {3.2}Syntax and Mobility}{8}{section.12}
\contentsline {section}{\numberline {3.3}An Example}{9}{section.16}
\contentsline {chapter}{\numberline {4}Methodology for JavaPict}{11}{chapter.19}
\contentsline {section}{\numberline {4.1}$\pi $-calculus and object oriented paradigm}{11}{section.20}
\contentsline {section}{\numberline {4.2}Software Transactional Memory(STM)}{12}{section.21}
\contentsline {section}{\numberline {4.3}JavaPict library}{14}{section.22}
\contentsline {section}{\numberline {4.4}Usage}{14}{section.23}
\contentsline {chapter}{\numberline {5}Type Soundness Proof}{16}{chapter.25}
\contentsline {section}{\numberline {5.1}Introduction}{16}{section.26}
\contentsline {section}{\numberline {5.2}Featherweight Generic Java (FGJ)}{17}{section.27}
\contentsline {subsection}{\numberline {5.2.1}Background}{17}{subsection.28}
\contentsline {subsection}{\numberline {5.2.2}FGJ definitions}{17}{subsection.29}
\contentsline {subsection}{\numberline {5.2.3}Syntax for FGJ}{18}{subsection.30}
\contentsline {chapter}{\numberline {6}Extending FGJ with JavaPict}{19}{chapter.32}
\contentsline {section}{\numberline {6.1}Introduction}{19}{section.33}
\contentsline {section}{\numberline {6.2}Syntax}{22}{section.34}
\contentsline {section}{\numberline {6.3}Auxiliary Functions}{23}{section.36}
\contentsline {section}{\numberline {6.4}Subtyping and Well-formedness}{23}{section.38}
\contentsline {section}{\numberline {6.5}Typing}{26}{section.40}
\contentsline {section}{\numberline {6.6}Reduction}{28}{section.42}
\contentsline {chapter}{\numberline {7}Conclusion and Future Work}{31}{chapter.44}
\contentsline {chapter}{Bibliography}{37}{chapter*.45}
\contentsline {chapter}{\numberline {A}FGJP Type Safety}{38}{appendix.46}
\contentsline {section}{\numberline {A.1}Proof of Theorem 6.6.1}{38}{section.47}
\contentsline {subsection}{\numberline {A.1.1}Weakening}{38}{subsection.48}
\contentsline {subsection}{\numberline {A.1.2}Inheritance transitivity}{39}{subsection.49}
\contentsline {subsection}{\numberline {A.1.3}Downcast property}{39}{subsection.50}
\contentsline {subsection}{\numberline {A.1.4}Downcast inequality}{39}{subsection.51}
\contentsline {subsection}{\numberline {A.1.5}Type substitution preserves subtyping}{39}{subsection.52}
\contentsline {subsection}{\numberline {A.1.6}Type substitution preserves well-formedness}{40}{subsection.53}
\contentsline {subsection}{\numberline {A.1.7}Bound property}{40}{subsection.54}
\contentsline {subsection}{\numberline {A.1.8}Fields of superclass are retained}{41}{subsection.55}
\contentsline {subsection}{\numberline {A.1.9}Method overriding}{41}{subsection.56}
\contentsline {subsection}{\numberline {A.1.10}Type substitution preserves Typing}{42}{subsection.57}
\contentsline {section}{\numberline {A.2}Term substitution preserves Typing}{42}{section.58}
\contentsline {section}{\numberline {A.3}Type substitution preserves method subtyping}{43}{section.59}
